/**************************************************************************
* File:            2sat.h	                                              *
* Description:	   Methods and structures to solve 2-SAT problem          *
* Author:          Zhuk Artsem, 399                                       *
**************************************************************************/
#pragma once

#include "graph.h"
#include "tarjan.h"

#include <vector>

struct Variable{
	int index_;
	bool desired_;
	Variable(){}
	Variable(int index, bool desired) :index_(index), desired_(desired){}
	int getNumber(){
		return 2 * index_ + desired_;
	}
	bool isTrue(bool value){
		return desired_== value;
	}
};

struct Disjunct{
	Variable x, y;
	Disjunct(){}
	Disjunct(int a, bool nega, int b, bool negb):x(a,nega),y(b,negb){}
	bool isFulfiled(bool valueX, bool valueY){
		return x.isTrue(valueX) || y.isTrue(valueY);
	}
};

int notVariable(int number){
	return number ^ 1;
}

int variableNumber(int number){
	return number / 2;
}

bool isNegation(int number){
	return number % 2 == 0;
}

std::unique_ptr<Graph> make2SATGraph(int variablesCount, std::vector<Disjunct> const &disjuncts){
	std::vector<Edge> edges;
	for (auto disjunct : disjuncts){
		int a = disjunct.x.getNumber();
		int b = disjunct.y.getNumber();
		edges.emplace_back(notVariable(a),b); 
		edges.emplace_back(notVariable(b),a); 
	}
	return makeCompactGraph(edges, variablesCount * 2);
}

std::vector<bool> get2SATSolution(int variablesCount, std::vector<Disjunct> const &disjuncts){
	std::unique_ptr<Graph> graph = make2SATGraph(variablesCount, disjuncts);
	std::vector<std::vector<int> > scc = getSCC(graph.get());
	std::vector<std::pair<int, int> > coloring;
	std::vector<bool> banned(scc.size());
	std::vector<int> color(2 * variablesCount);
	std::vector<bool> value(variablesCount);
	std::vector<bool> setted(variablesCount);

	for (int i = 0; i < scc.size(); ++i)
		for (int x : scc[i]){
			coloring.emplace_back(i, x);
			color[x] = i;
		}

	std::sort(coloring.begin(), coloring.end());

	for (auto term : coloring){
		int currentColor = term.first;
		int index = variableNumber(term.second);

		if (banned[currentColor])
			continue;
		
		value[index] = !isNegation(term.second);
		setted[index] = true;

		banned[color[notVariable(term.second)]] = true;
	}

	for (int i = 0; i < variablesCount; ++i)
	if (!setted[i])
		return std::vector<bool>();

	return value;
}

